/-
Copyright (c) 2025 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.AlgebraicTopology.SimplicialSet.Basic
import Mathlib.CategoryTheory.Subpresheaf.OfSection

/-!
# Subcomplexes of a simplicial set

Given a simplicial set `X`, this file defines the type `X.Subcomplex`
of subcomplexes of `X` as an abbreviation for `Subpresheaf X`.
It also introduces a coercion from `X.Subcomplex` to `SSet`.

## Implementation note

`SSet.{u}` is defined as `Cᵒᵖ ⥤ Type u`, but it is not an abbreviation.
This is the reason why `Subpresheaf.ι` is redefined here as `Subcomplex.ι`
so that this morphism appears as a morphism in `SSet` instead of a morphism
in the category of presheaves.

-/

universe u

open CategoryTheory Simplicial

namespace SSet

-- Note: this could be obtained as `inferInstanceAs (Balanced (_ ⥤ _))`
-- by importing `Mathlib.CategoryTheory.Adhesive`, but we give a
-- different proof so as to reduce imports
instance : Balanced SSet.{u} where
  isIso_of_mono_of_epi f _ _ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro
    rw [isIso_iff_bijective]
    constructor
    · rw [← mono_iff_injective]
      infer_instance
    · rw [← epi_iff_surjective]
      infer_instance

variable (X Y : SSet.{u})

/-- The complete lattice of subcomplexes of a simplicial set. -/
abbrev Subcomplex := Subpresheaf X

variable {X Y}

namespace Subcomplex

/-- The underlying simplicial set of a subcomplex. -/
abbrev toSSet (A : X.Subcomplex) : SSet.{u} := A.toPresheaf

instance : CoeOut X.Subcomplex SSet.{u} where
  coe := fun S ↦ S.toSSet

/-- If `A : Subcomplex X`, this is the inclusion `A ⟶ X` in the category `SSet`. -/
abbrev ι (A : Subcomplex X) : Quiver.Hom (V := SSet) A X := Subpresheaf.ι A

instance (A : X.Subcomplex) : Mono A.ι :=
  inferInstanceAs (Mono (Subpresheaf.ι A))

/-- The subcomplex of a simplicial set that is generated by a simplex. -/
abbrev ofSimplex {n : ℕ} (x : X _⦋n⦌) : X.Subcomplex := Subpresheaf.ofSection x

lemma mem_ofSimplex_obj {n : ℕ} (x : X _⦋n⦌) :
    x ∈ (ofSimplex x).obj _ :=
  Subpresheaf.mem_ofSection_obj x

lemma ofSimplex_le_iff {n : ℕ} (x : X _⦋n⦌) (A : X.Subcomplex) :
    ofSimplex x ≤ A ↔ x ∈ A.obj _ :=
  Subpresheaf.ofSection_le_iff _ _

lemma mem_ofSimplex_obj_iff {n : ℕ} (x : X _⦋n⦌) {m : SimplexCategoryᵒᵖ} (y : X.obj m) :
    y ∈ (ofSimplex x).obj m ↔ ∃ (f : m.unop ⟶ ⦋n⦌), X.map f.op x = y := by
  dsimp [ofSimplex, Subpresheaf.ofSection]
  aesop

section

variable (f : X ⟶ Y)

/-- The range of a morphism of simplicial sets, as a subcomplex. -/
abbrev range : Y.Subcomplex := Subpresheaf.range f

/-- The morphism `X ⟶ Subcomplex.range f` induced by `f : X ⟶ Y`. -/
abbrev toRange : X ⟶ Subcomplex.range f := Subpresheaf.toRange f

@[reassoc (attr := simp)]
lemma toRange_ι : toRange f ≫ (Subcomplex.range f).ι = f := rfl

@[simp]
lemma toRange_app_val {Δ : SimplexCategoryᵒᵖ} (x : X.obj Δ) :
    ((toRange f).app Δ x).val = f.app Δ x := rfl

instance : Epi (toRange f) :=
  inferInstanceAs (Epi (Subpresheaf.toRange f))

instance [Mono f] : Mono (toRange f) :=
  mono_of_mono_fac (toRange_ι f)

instance [Mono f] : IsIso (toRange f) :=
  isIso_of_mono_of_epi _

end

end Subcomplex

end SSet
